\documentclass{article} 
\usepackage{url} 
\usepackage{hyperref}
\usepackage{stmaryrd}
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{savesym}
\usepackage{amssymb} 
%% \savesymbol{mathfrak}
%\usepackage{MnSymbol} Overall mnsymbol is depressing.
%\restoresymbol{MN}{mathfrak}
\usepackage{xcolor} 
%\usepackage{mathrsfs}
\usepackage{amsmath, amsthm}
%\usepackage{diagrams}
\makeatletter
\newsavebox{\@brx}
\newcommand{\llangle}[1][]{\savebox{\@brx}{\(\m@th{#1\langle}\)}%
  \mathopen{\copy\@brx\kern-0.6\wd\@brx\usebox{\@brx}}}
\newcommand{\rrangle}[1][]{\savebox{\@brx}{\(\m@th{#1\rangle}\)}%
  \mathclose{\copy\@brx\kern-0.6\wd\@brx\usebox{\@brx}}}
\makeatother


\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 

\newcommand{\mlstep}[1]{\twoheadrightarrow_{\underline{#1}}}
\newcommand{\lstep}[1]{\to_{\underline{#1}}}
\newcommand{\mstep}[1]{\twoheadrightarrow_{#1}}
\newcommand{\ep}[0]{\epsilon} 
\newcommand{\nil}[0]{\mathsf{nil}} 
\newcommand{\cons}[0]{\mathsf{cons}} 
\newcommand{\vecc}[0]{\mathsf{vec}} 
\newcommand{\suc}[0]{\mathsf{S}} 
\newcommand{\app}[0]{\mathsf{app}} 
\newcommand{\interp}[1]{\llbracket #1 \rrbracket} 
\newcommand{\intern}[1]{\llangle #1 \rrangle} 
\newcommand*\template[1]{\(\langle\)#1\(\rangle\)}
%% \newarrowfiller{dasheq} {==}{==}{==}{==}
%% \newarrow {Mapsto} |--->
%% \newarrow {Line} -----
%% \newarrow {Implies} ===={=>}
%% \newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
%% \newarrow {Onto} ----{>>}
%% \newarrow {Dashto}{}{dash}{}{dash}{>}
%% \newarrow {Dashtoo}{}{dash}{}{dash}{>>}

\newtheorem{prop}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}


\begin{document}
%\pagestyle{empty}
\title{Interior Semantics for Equality}
\author{Peng Fu \\
Computer Science, The University of Iowa}
\date{Last edited: \today}


\maketitle \thispagestyle{empty}


\section{A Nontarskian Style Semantics}
Given a formula $a = b$, what do you make of it? The Tarskian answer is 
$\interp{a} \dot{=} \interp{b}$, where $\interp{a}, \dot{=}, \interp{b}$ all are
in a metalanguage. And $\dot{=}$ expresses a notion of equality within the metalanguage. Let us 
forget the philosophical arguments for whether or not Tarskian style semantics is adequate, but explore another point of view on the semantics that is not Tarskian style. Let us restrict ourself in $\mathfrak{G}$. We would define $a = b := \Pi X. (a \ep X \to b \ep X)$. So we would say the semantics of $a = b$ is a formula about $a, b$, namely, $\Pi X. (a \ep X \to b \ep X)$. I will call this style of semantics \textit{interior semantics}. The motivation for this new style of semantics is when we give \textit{meaning} to certain \textit{concepts}, the meaning should
not appeal to the \textit{concepts} themself. 

Tarskian semantics follows this tradition, but it
does not specify what exactly the meta-language is and the explanation of $\dot{=}$ then has to appeals to certain intuition about equality, namely, it has to specify an notion of equivalent relation. When asked what do you mean by an equivalent relation, then Tarskian will say it is a reflexive, symmetric and transitive relation. This is unacceptable in the sense that one veiw the reflexive, symmetric and transitive relation as the consequence of $=$. So Tarskian style semantics inevitably leads to \textit{circular explanation}.   

Interior semantics in this sense is better, because, indeed, from the semantics of $a = b$(a.k.a. $\Pi X. (a \ep X \to b \ep X)$), one can indeed prove that $=$ is a the reflexive, symmetric and transitive relation. And we say all the propertes that we can prove about $=$ in $\mathfrak{G}$ \textit{manifests} the meaning of $=$. \textit{Operationally}, if one has a proof $p$ of a formula about $a$
(denoted by $F[a]$), then we would expect we will have another proof $p'$ of $F[b]$ will hold (if we take the strongest notion of equality ). Indeed, this behavior give rise of the notion of operational semantics, namely, if one attach a lambda term to each proof(denoted by $t_p$) in the style of $\mathfrak{G}$, then one would have $t_p =_{\beta} t_{p'}$.  

\section{More Expositions on $\mathfrak{G}$}

In fact, we set up $\mathfrak{G}$ in a way that it does not distinguish beta equal terms(beta equal terms are intensionaly equal in $\mathfrak{G}$), this allows an external computational power comes in. 


\cite{Church:1985}
\bibliographystyle{plain}
\bibliography{meaning-eq}

\appendix

\end{document}
